/***************************************************************************
 * File name: q3.c
 *
 * Authors:  Tomer Filiba		Reuven Horon
 *           037013075			066729740
 *           sebulba@t2			sreuvenh@t2
 *
 * Exercise #: 6
 * Question #: 3
 * Submission Date: 29/8/07
 **************************************************************************/

/*-------------------------------------------------------------------------
  Include files:
--------------------------------------------------------------------------*/
#include <stdio.h>
#include <stdlib.h>

/*=========================================================================
  Constants and definitions:
==========================================================================*/
#define VARS_NUM    5
#define CLAUSES_NUM 4

typedef enum {
	FALSE = -1, 
	UNSET = 0, 
	TRUE=1
} truth;


/*=========================================================================
  Forward declarations:
==========================================================================*/
truth dpll(truth cnf[CLAUSES_NUM][VARS_NUM], truth assignment[VARS_NUM]);
truth cnf_sat(truth cnf[CLAUSES_NUM][VARS_NUM], truth assignment[VARS_NUM]);
truth clause_sat(truth clause[VARS_NUM], truth assignment[VARS_NUM]);
int next_literal(truth cnf[CLAUSES_NUM][VARS_NUM], truth assignment[VARS_NUM]);
void print_cnf(truth cnf[CLAUSES_NUM][VARS_NUM], truth assignment[VARS_NUM], truth cnf_truth);
void printf_cnf_formula(truth cnf[CLAUSES_NUM][VARS_NUM]);
void print_assignment(truth assignment[VARS_NUM]);


/*-------------------------------------------------------------------------
  The main program.

  The program tries to find an assingment which gives TRUE to a CNF formula.
  The CNF formula is defined by the array cnf[CLAUSES_NUM][VARS_NUM].
  The result assignment should be presented in the array assignment[VARS_NUM],
  and to be printed.

  The program implements the DPLL algorithm for finding the requested 
  assignment.
 -------------------------------------------------------------------------*/
int main()
{
    truth cnf_truth = UNSET;
    truth assignment[VARS_NUM] = {0};
    truth cnf[CLAUSES_NUM][VARS_NUM] = {{0,  1,  0,  0,  1},
	                                    {1,  0, -1, -1,  0},
	  									{0,  0,  0,  0, -1},
	                                    {1, -1,  0,  1, -1}};
	
    cnf_truth = dpll(cnf, assignment);
    print_cnf(cnf, assignment, cnf_truth);
    return 0;
}

/*-------------------------------------------------------------------------
  Finds an assignment which gives the value TRUE to the given CNF formula,
  by implementing the DPLL algorithm.
  
  Parameters:
  truth cnf[CLAUSES_NUM][VARS_NUM]- the CNF formula
  truth assignment[VARS_NUM]      - the array in which the result assignment 
									should be written to. In the call to the
									fucntion, it represents a partial assignment

  Return value: TRUE  - if the function found a requested assignment
				FALSE - if the function did not find such assignment
    
  Special Notes: The function is recursive. In each call, it takes the 
				 partial assignment given by the array assignment, and adds 
				 another variable assignment to it.
 -------------------------------------------------------------------------*/
truth dpll(truth cnf[CLAUSES_NUM][VARS_NUM], truth assignment[VARS_NUM])
{
	int i;
	
    truth state = cnf_sat(cnf, assignment);
    if (state != UNSET)
        return state;
	
	/* find next literal to assign (or give up if we reached the end) */
	i = next_literal(cnf, assignment);
	if (i == -1)
		return FALSE;
	
    assignment[i] = FALSE;
    if (dpll(cnf, assignment) == TRUE)
        return TRUE;
	
    assignment[i] = TRUE;
    if (dpll(cnf, assignment) == TRUE)
        return TRUE;
	
    assignment[i] = UNSET;
    return FALSE;
}

/*-------------------------------------------------------------------------
  The unit-propagation algorithm: determines the best literal to assign to,
  so as to "chop" down the useless branches of the search tree as soon as
  possible. the algorithm is as follows: iterate over all CNF clauses,
  and find the first clause that has only one unassigned literal in it,
  and choose this unassigned as the next literal to assign. if there are 
  no such clauses, just return the next free literal. if there are no
  free literals at all, return -1.
  
  Parameters:
  truth cnf[CLAUSES_NUM][VARS_NUM]- the CNF formula
  truth assignment[VARS_NUM]      - the array of the current partial 
                                    assignment
  
  Return value: the index of the best literal to assign to. if there are no
  free literals left, returns -1.
 -------------------------------------------------------------------------*/
int next_literal(truth cnf[CLAUSES_NUM][VARS_NUM], truth assignment[VARS_NUM])
{
	int i, j, res, free_count;
	
	for (i = 0; i < CLAUSES_NUM; i++) {
		free_count = 0;
		for (j = 0; j < VARS_NUM; j++) {
			/* is there a required literal that is not yet assigned ? */
			if (cnf[i][j] != 0 && assignment[j] == 0) {
				free_count += 1;
				res = j;
			}
		}
		/* if there is only one such literal -- jackpot */
		if (free_count == 1)
			return res;
	}
	
	/* no unit propagation was detected, just return the next free literal */
	for (i = 0; i < VARS_NUM; i++) {
		if (assignment[i] == 0)
			return i;
	}
	
	/* no free literals */
	return -1;
}


/*-------------------------------------------------------------------------
  The function finds out what truth value does the given CNF formula has 
  when assigning to it the given assignment. 
    
  Parameters:
  truth cnf[CLAUSES_NUM][VARS_NUM]- the CNF formula
  truth assignment[VARS_NUM]      - the assignment to be checked on the
									CNF formula

  Return value: TRUE  - if the assignment gives the value TRUE to the CNF
					    formula. 
				FALSE - if the assignment gives the value FALSE to the CNF
					    formula. 
				UNSET - if the assigment is a partial assignment, and the 
				        value of the CNF formula is not determined by the
						assigned variables.
    
  Special Notes: The assignment can be a partial assignmet.
 -------------------------------------------------------------------------*/
truth cnf_sat(truth cnf[CLAUSES_NUM][VARS_NUM], truth assignment[VARS_NUM])
{
    truth clause_truth = UNSET, t = TRUE;
    int i = 0;
	
    for (i = 0; i < CLAUSES_NUM; i++)
    {
        clause_truth = clause_sat(cnf[i], assignment);
        if (clause_truth == FALSE)
            return FALSE;
        if (clause_truth == UNSET)
            t = UNSET;
    }
    return t;
}

/*-------------------------------------------------------------------------
  The function finds out what truth value does the given clause has 
  when assigning to it the given assignment. 
    
  Parameters:
  truth clause[VARS_NUM]     - the checked clause
  truth assignment[VARS_NUM] - the assignment to be checked on the clause

  Return value: TRUE  - if the assignment gives the value TRUE to the clause
				FALSE - if the assignment gives the value FALSE to the clause
				UNSET - if the assigment is a partial assignment, and the 
				        value of the clause is not determined by the
						assigned variables.
    
  Special Notes: The assignment can be a partial assignmet.
 -------------------------------------------------------------------------*/
truth clause_sat(truth clause[VARS_NUM], truth assignment[VARS_NUM])
{
    truth t = FALSE;
    int i;
	
    for (i = 0; i < VARS_NUM; i++)
    {
        if (clause[i] != 0) 
        {
            if (assignment[i] == clause[i])
                return TRUE;
            if (assignment[i] == UNSET)
                t = UNSET;
        }
    }
    return t;
}

/*-------------------------------------------------------------------------
  Printing functions:
--------------------------------------------------------------------------*/

/*-------------------------------------------------------------------------
  The function prints the given CNF formula, and the assignment given to it
  if it satisfies it (if it gives it the value TRUE)
    
  Parameters:
  truth cnf[CLAUSES_NUM][VARS_NUM] - the CNF formula
  truth assignment[VARS_NUM]       - the assignment
  truth cnf_truth                  - the value the given assignmnet has when 
                                     assigning it to the given CNF formula.

  Return value: void
    
  Special Notes: none
 -------------------------------------------------------------------------*/
void print_cnf(truth cnf[CLAUSES_NUM][VARS_NUM], truth assignment[VARS_NUM], truth cnf_truth)
{
    printf("The CNF Fomula:\n");
    printf_cnf_formula(cnf);
	printf("\n");

    switch (cnf_truth)
    {
    case FALSE: 
		printf("cannot be satisfied\n");
        break;
    case UNSET: 
		/* Error: the result of dpll() should be TRUE or FALSE only */
		printf("was not checked to be satisfied or not\n"); 
        break;
    case TRUE:  
		printf("can be satisfied with the assignment:\n");
        print_assignment(assignment);
        printf("\n");
        break;
    } 
}

/*-------------------------------------------------------------------------
  The function prints the given CNF formula
    
  Parameters:
  truth cnf[CLAUSES_NUM][VARS_NUM] - the CNF formula

  Return value: void
    
  Special Notes: none
 -------------------------------------------------------------------------*/
void printf_cnf_formula(truth cnf[CLAUSES_NUM][VARS_NUM])
{
    int ci=0, vi=0, printOrFlag=0;

    for (ci=0; ci<CLAUSES_NUM; ci++)
    {
        printOrFlag=0;
        printf("(");
        for (vi=0; vi<VARS_NUM; vi++)
        {
            if (cnf[ci][vi] == 0)
                continue;

            // print OR only if at least one variable was printed
            if (printOrFlag) 
                printf(" OR ");

            if (cnf[ci][vi] == -1)
                printf("!");
            printf("x%d", vi);
            printOrFlag = 1;
        }
        printf(")");
        if (ci < CLAUSES_NUM-1) // don't print AND after the last clause
            printf(" AND ");
    }
    printf("\n");
}

/*-------------------------------------------------------------------------
  The function prints the given assignment
    
  Parameters:
  truth assignment[VARS_NUM] - the assignment

  Return value: void
    
  Special Notes: 
 -------------------------------------------------------------------------*/
void print_assignment(truth assignment[VARS_NUM])
{
    int vi=0;
    for (vi=0; vi<VARS_NUM; vi++)
    {
        printf("x%d = ", vi);
        switch (assignment[vi])
        {
        case FALSE: printf("FALSE"); break;
        case UNSET: printf("UNSET"); break;
        case TRUE:  printf("TRUE"); break;
        }
        if (vi < VARS_NUM-1) // don't print "," after the last variable
            printf(", ");
    }
    printf("\n");
}

/**************************************************************************
			                          End of file
***************************************************************************/